AWS-LC is Amazon’s open-source cryptographic library, powering billions of daily cryptographic operations across security-critical AWS services. As the cryptographic foundation for AWS, the library undergoes yearly FIPS validation and demands the highest levels of assurance. With the threat of “store now, decrypt later” quantum attacks driving AWS’s post-quantum migration plan, integrating high-assurance ML-KEM support into AWS-LC has been a critical priority. This talk describes how we developed and integrated mlkem-native, an optimized and formally verified ML-KEM implementation developed under the Post-Quantum Cryptography Alliance (PQCA), into AWS-LC. Building on the ML-KEM reference implementation, mlkem-native adds optimized assembly backends achieving 2.08x-2.78x performance improvements on Graviton processors and 1.5x-2.0x on x86, while providing formal verification guarantees across both C and assembly layers. This implementation is now part of AWS-LC’s 2025-2026 FIPS validation cycle.

AWS-LC’s reach extends well beyond AWS services. Through aws-lc-rs, a Rust cryptographic library built on AWS-LC, it serves as the default cryptographic provider for rustls, a widely adopted TLS library. The underlying mlkem-native implementation has also been adopted as the default ML-KEM in libOQS, part of the Open Quantum Safe project.

We discuss our verification strategy: CBMC verifies the C code for memory-safety, type-safety, and in some cases functional correctness, using contracts and loop invariants, while HOL Light verifies the hand-crafted assembly for functional correctness using the s2n-bignum infrastructure. We explain how these verification domains connect at the C-assembly boundary, how we keep proofs synchronized with code through CI, and our ongoing work on constant-time verification. We reflect on lessons learned from deploying formally verified post-quantum cryptography into a production library at AWS scale.

NOTE: At some points this video blanks briefly to a white screen to obscure attendees with red lanyards who did not consent to being recorded.

plus-circle Add Review

comment

Reviews